(declare-const v2 Bool)
(declare-const v5 Bool)
(declare-const i0 Int)
(declare-const i1 Int)
(declare-const i7 Int)
(declare-const i8 Int)
(declare-const i9 Int)
(declare-const i10 Int)
(declare-const i14 Int)
(declare-const i16 Int)
(declare-const v16 Bool)
(declare-const i20 Int)
(assert (<= (div i10 38) (- 4)))
(assert (or v2 v5))
(assert (or (=> v16 (distinct 17 47 (* i9 (- 71)) i0))))
(assert (< 40 i9))
(check-sat)
